#include "PDTSpecCheck.h"
#include "PDTCodeGraph.h"
#include "PDTFunction.h"
#include "PDTCondition.h"
#include "PDTBehavior.h"
#include "PDTType.h"
#include "PDTNumVar.h"
#include "PDTNumConst.h"
#include "PDTExp.h"

void 
PDTSpecCheck::
buildGoodRanges(PDTFunctionDec & functionDec, 
        PDTBehaviors& behaviors,
        string funcName, 
        vector <PDTIntRange*> & ranges, 
        vector <PDTVar*> & variables)
{
    vector <PDTBehavior*> goodAssignments;
    behaviors.getGoodAssignments(goodAssignments); //All good behaviors
    int** listOfMinimums = new int*[goodAssignments[0]->wholeSize()];
    int** listOfMaximums = new int*[goodAssignments[0]->wholeSize()];

    for (int i = 0; i<goodAssignments[0]->wholeSize(); i++)
    {
        listOfMinimums[i] = NULL;
        listOfMaximums[i] = NULL;
    }

    for (unsigned int i = 0; i<goodAssignments.size(); i++) //loop over all behaviors
    {
        vector <PDTNode*> allExpressions;
        goodAssignments[i]->getAllExpressions(allExpressions);
        vector <PDTVar*> allVars;
        goodAssignments[i]->getAllVariables(allVars);

        //loop over all the variables
        for (unsigned int j = 0; j<allExpressions.size(); j++) // allExpressions and allVariables have the same size
        {
            if (allExpressions[j]->isConstSequence()) //if sequence assign
            {
                PDTConstSequence* cSeq = dynamic_cast<PDTConstSequence*>(allExpressions[j]);
                for (unsigned int k = 0; k<cSeq->getSize(); k++)
                {
                    PDTNode* elem = cSeq->getElementAt(k);
                    elem->eval(*CG);
                    PDTNumConstInt* intElem = dynamic_cast<PDTNumConstInt*>(elem->nValue);
                    if (listOfMinimums[j] == NULL)
                        listOfMinimums[j] = new int(intElem->getValue());
                    else if (intElem->getValue()<*listOfMinimums[j])
                        *(listOfMinimums[j]) = intElem->getValue();

                    if (listOfMaximums[j] == NULL)
                        listOfMaximums[j] = new int(intElem->getValue());
                    else if (intElem->getValue()>*listOfMaximums[j])
                        *(listOfMaximums[j]) = intElem->getValue();
                }

            }
            else //if single variable assign
            {
                allExpressions[j]->eval(*CG);
                PDTNumConstInt* value = dynamic_cast<PDTNumConstInt*>(allExpressions[j]->nValue);
                if (listOfMinimums[j] == NULL)
                    listOfMinimums[j] = new int(value->getValue());
                else if (value->getValue()<*listOfMinimums[j])
                    *(listOfMinimums[j]) = value->getValue();

                if (listOfMaximums[j] == NULL)
                    listOfMaximums[j] = new int(value->getValue());
                else if (value->getValue()>*listOfMaximums[j])
                    *(listOfMaximums[j]) = value->getValue();

            }
        }
    }
    variables = goodAssignments[0]->getAllVariables(variables);
    PDTNumConstInt* valMin;
    PDTNumConstInt* valMax;
    for (int i = 0; i<goodAssignments[0]->wholeSize(); i++)
    {
        valMin = new PDTNumConstInt(*CG, *(listOfMinimums[i]));
        PDTExp* valMinExp = dynamic_cast<PDTExp*>(valMin);
        valMax = new PDTNumConstInt(*CG, *(listOfMaximums[i]));
        PDTExp* valMaxExp = dynamic_cast<PDTExp*>(valMax);
        PDTIntRange *range = new PDTIntRange(*CG, " ", valMinExp, valMaxExp);
        ranges.push_back(range);
    }
    stringstream ss(stringstream::in | stringstream::out);
    ss<<endl;
    ss<<"==================================================================="<<endl;
    ss<<"            Building Ranges based on 'GOOD' Behaviors.             "<<endl;
    ss<<"==================================================================="<<endl;
    for (int i = 0; i<goodAssignments[0]->wholeSize(); i++)
    {
        ss<<"variable "<<variables[i]->getName()<<" has the following range: ";
        ranges[i]->getStart()->eval(*CG);
        ranges[i]->getEnd()->eval(*CG);
        ss<<"["<<((PDTNumConstInt*)(ranges[i]->getStart()))->getValue()<<" .. "<<((PDTNumConstInt*)(ranges[i]->getEnd()))->getValue()<<"]"<<endl;
    }
    ss<<"==================================================================="<<endl;
    cout<<ss.str()<<endl;
}


void 
PDTSpecCheck::
buildBadRanges(PDTFunctionDec & functionDec,
        PDTBehaviors & behaviors,
        string funcName, 
        vector <PDTIntRange*> & ranges, 
        vector <PDTVar*> & variables)
{
	vector <PDTBehavior*> badAssignments;
	behaviors.getBadAssignments(badAssignments); //All bad behaviors

	int** listOfMinimums;
	listOfMinimums = new int*[badAssignments[0]->wholeSize()];
	int** listOfMaximums;
	listOfMaximums = new int*[badAssignments[0]->wholeSize()];

	for (int i = 0; i<badAssignments[0]->wholeSize(); i++)
	{
		listOfMinimums[i] = NULL;
		listOfMaximums[i] = NULL;
	}

	for (unsigned int i = 0; i<badAssignments.size(); i++) //loop over all behaviors
	{
		vector <PDTNode*> allExpressions;
		allExpressions = badAssignments[i]->getAllExpressions(allExpressions);
		vector <PDTVar*> allVars;
		allVars = badAssignments[i]->getAllVariables(allVars);

		//loop over all the variables
		for (unsigned int j = 0; j<allExpressions.size(); j++) // allExpressions and allVariables have the same size
		{
			if (allExpressions[j]->isConstSequence()) //if sequence assign
			{
				PDTConstSequence* cSeq = dynamic_cast<PDTConstSequence*>(allExpressions[j]);
				for (unsigned int k = 0; k<cSeq->getSize(); k++)
				{
					PDTNode* elem = cSeq->getElementAt(k);
					elem->eval(*CG);
					PDTNumConstInt* intElem = dynamic_cast<PDTNumConstInt*>(elem->nValue);
					if (listOfMinimums[j] == NULL)
						listOfMinimums[j] = new int(intElem->getValue());
					else if (intElem->getValue()<*listOfMinimums[j])
						*(listOfMinimums[j]) = intElem->getValue();

					if (listOfMaximums[j] == NULL)
						listOfMaximums[j] = new int(intElem->getValue());
					else if (intElem->getValue()>*listOfMaximums[j])
						*(listOfMaximums[j]) = intElem->getValue();
				}
			}
			else //if single variable assign
			{
				allExpressions[j]->eval(*CG);
				PDTNumConstInt* value = dynamic_cast<PDTNumConstInt*>(allExpressions[j]->nValue);
				if (listOfMinimums[j] == NULL)
					listOfMinimums[j] = new int(value->getValue());
				else if (value->getValue()<*listOfMinimums[j])
					*(listOfMinimums[j]) = value->getValue();

				if (listOfMaximums[j] == NULL)
					listOfMaximums[j] = new int(value->getValue());
				else if (value->getValue()>*listOfMaximums[j])
					*(listOfMaximums[j]) = value->getValue();
			}
		}
	}
	variables = badAssignments[0]->getAllVariables(variables);
	PDTNumConstInt* valMin;
	PDTNumConstInt* valMax;
	for (int i = 0; i<badAssignments[0]->wholeSize(); i++)
	{
		valMin = new PDTNumConstInt(*CG, *(listOfMinimums[i]));
		PDTExp* valMinExp = dynamic_cast<PDTExp*>(valMin);
		valMax = new PDTNumConstInt(*CG, *(listOfMaximums[i]));
		PDTExp* valMaxExp = dynamic_cast<PDTExp*>(valMax);
		PDTIntRange *range = new PDTIntRange(*CG, " ", valMinExp, valMaxExp);
		ranges.push_back(range);
	}
	stringstream ss(stringstream::in | stringstream::out);
	ss<<endl;
	ss<<"==================================================================="<<endl;
	ss<<"            Building Ranges based on 'BAD' Behaviors.              "<<endl;
	ss<<"==================================================================="<<endl;
	for (int i = 0; i<badAssignments[0]->wholeSize(); i++)
	{
		ss<<"variable "<<variables[i]->getName()<<" has the following range: ";
		ranges[i]->getStart()->eval(*CG);
		ranges[i]->getEnd()->eval(*CG);
		ss<<"["<<((PDTNumConstInt*)(ranges[i]->getStart()))->getValue()<<" .. "<<((PDTNumConstInt*)(ranges[i]->getEnd()))->getValue()<<"]"<<endl;
	}
	ss<<"==================================================================="<<endl;
	cout<<ss.str()<<endl;
}

void 
PDTSpecCheck::
buildAllRanges(PDTFunctionDec& functionDec,
        PDTBehaviors & behaviors,
        const string & funcName, 
        vector <PDTIntRange*> &ranges, 
        vector <PDTVar*> & variables)
{
	vector <PDTBehavior*> goodAssignments;
	behaviors.getGoodAssignments(goodAssignments); //All good behaviors

	vector <PDTBehavior*> badAssignments;
	behaviors.getBadAssignments(badAssignments); //All bad behaviors

	int** listOfMinimums;
	listOfMinimums = new int*[goodAssignments[0]->wholeSize()];
	int** listOfMaximums;
	listOfMaximums = new int*[goodAssignments[0]->wholeSize()];

	for (int i = 0; i<goodAssignments[0]->wholeSize(); i++)
	{
		listOfMinimums[i] = NULL;
		listOfMaximums[i] = NULL;
	}

	for (unsigned int i = 0; i<goodAssignments.size(); i++) //loop over good all behaviors
	{
		vector <PDTNode*> allExpressions;
		goodAssignments[i]->getAllExpressions(allExpressions);
		vector <PDTVar*> allVars;
		goodAssignments[i]->getAllVariables(allVars);

		//loop over all the variables
		for (unsigned int j = 0; j<allExpressions.size(); j++) // allExpressions and allVariables have the same size
		{
			if (allExpressions[j]->isConstSequence()) //if sequence assign
			{
				PDTConstSequence* cSeq = dynamic_cast<PDTConstSequence*>(allExpressions[j]);
				for (unsigned int k = 0; k<cSeq->getSize(); k++)
				{
					PDTNode* elem = cSeq->getElementAt(k);
					elem->eval(*CG);
					PDTNumConstInt* intElem = dynamic_cast<PDTNumConstInt*>(elem->nValue);
					if (listOfMinimums[j] == NULL)
						listOfMinimums[j] = new int(intElem->getValue());
					else if (intElem->getValue()<*listOfMinimums[j])
						*(listOfMinimums[j]) = intElem->getValue();

					if (listOfMaximums[j] == NULL)
						listOfMaximums[j] = new int(intElem->getValue());
					else if (intElem->getValue()>*listOfMaximums[j])
						*(listOfMaximums[j]) = intElem->getValue();
				}
			}
			else //if single variable assign
			{
				allExpressions[j]->eval(*CG);
				PDTNumConstInt* value = dynamic_cast<PDTNumConstInt*>(allExpressions[j]->nValue);
				if (listOfMinimums[j] == NULL)
					listOfMinimums[j] = new int(value->getValue());
				else if (value->getValue()<*listOfMinimums[j])
					*(listOfMinimums[j]) = value->getValue();

				if (listOfMaximums[j] == NULL)
					listOfMaximums[j] = new int(value->getValue());
				else if (value->getValue()>*listOfMaximums[j])
					*(listOfMaximums[j]) = value->getValue();
			}
		}
	}

	for (unsigned int i = 0; i<badAssignments.size(); i++) //loop over bad all behaviors
	{
		vector <PDTNode*> allExpressions;
		allExpressions = badAssignments[i]->getAllExpressions(allExpressions);
		vector <PDTVar*> allVars;
		allVars = badAssignments[i]->getAllVariables(allVars);

		//loop over all the variables
		for (unsigned int j = 0; j<allExpressions.size(); j++) // allExpressions and allVariables have the same size
		{
			if (allExpressions[j]->isConstSequence()) //if sequence assign
			{
				PDTConstSequence* cSeq = dynamic_cast<PDTConstSequence*>(allExpressions[j]);
				for (unsigned int k = 0; k<cSeq->getSize(); k++)
				{
					PDTNode* elem = cSeq->getElementAt(k);
					elem->eval(*CG);
					PDTNumConstInt* intElem = dynamic_cast<PDTNumConstInt*>(elem->nValue);
					if (listOfMinimums[j] == NULL)
						listOfMinimums[j] = new int(intElem->getValue());
					else if (intElem->getValue()<*listOfMinimums[j])
						*(listOfMinimums[j]) = intElem->getValue();

					if (listOfMaximums[j] == NULL)
						listOfMaximums[j] = new int(intElem->getValue());
					else if (intElem->getValue()>*listOfMaximums[j])
						*(listOfMaximums[j]) = intElem->getValue();
				}
			}
			else //if single variable assign
			{
				allExpressions[j]->eval(*CG);
				PDTNumConstInt* value = dynamic_cast<PDTNumConstInt*>(allExpressions[j]->nValue);
				if (listOfMinimums[j] == NULL)
					listOfMinimums[j] = new int(value->getValue());
				else if (value->getValue()<*listOfMinimums[j])
					*(listOfMinimums[j]) = value->getValue();

				if (listOfMaximums[j] == NULL)
					listOfMaximums[j] = new int(value->getValue());
				else if (value->getValue()>*listOfMaximums[j])
					*(listOfMaximums[j]) = value->getValue();
			}
		}
	}

	variables = goodAssignments[0]->getAllVariables(variables);
	PDTNumConstInt* valMin;
	PDTNumConstInt* valMax;
	for (int i = 0; i<goodAssignments[0]->wholeSize(); i++)
	{
		valMin = new PDTNumConstInt(*CG, *(listOfMinimums[i]));
		PDTExp* valMinExp = dynamic_cast<PDTExp*>(valMin);
		valMax = new PDTNumConstInt(*CG, *(listOfMaximums[i]));
		PDTExp* valMaxExp = dynamic_cast<PDTExp*>(valMax);
		PDTIntRange *range = new PDTIntRange(*CG, " ", valMinExp, valMaxExp);
		ranges.push_back(range);
	}
	stringstream ss(stringstream::in | stringstream::out);
	ss<<endl;
	ss<<"==================================================================="<<endl;
	ss<<"            Building Ranges based on 'ALL' Behaviors.              "<<endl;
	ss<<"==================================================================="<<endl;
	for (int i = 0; i<goodAssignments[0]->wholeSize(); i++)
	{
		ss<<"variable "<<variables[i]->getName()<<" has the following range: ";
		ranges[i]->getStart()->eval(*CG);
		ranges[i]->getEnd()->eval(*CG);
		ss<<"["<<((PDTNumConstInt*)(ranges[i]->getStart()))->getValue()<<" .. "<<((PDTNumConstInt*)(ranges[i]->getEnd()))->getValue()<<"]"<<endl;
	}
	ss<<"==================================================================="<<endl;
	cout<<ss.str()<<endl;
}

void PDTSpecCheck::checkGood(PDTFunctionDec& functionDec,
        PDTPreCondition& preCondition,
        PDTPostCondition& postCondition,
        PDTBehaviors& behaviors,
        const string & funcName, 
        int behaviorID)
{
	behaviors.assignGoodInput(*CG, behaviorID);
	preCondition.eval(*CG);
	behaviors.assignGoodOutput(*CG, behaviorID);
	postCondition.eval(*CG);

	//SPEC CHECK:
	bool PofI = (dynamic_cast<PDTBoolConst*>(preCondition.nValue))->getValue();
	bool QofO = (dynamic_cast<PDTBoolConst*>(postCondition.nValue))->getValue();
	stringstream ss(stringstream::in | stringstream::out);
	ss<<endl;
	ss<<"============"<<endl;
	ss<<"Final Result"<<endl;
	ss<<"============"<<endl;
	ss<<"Spec Check result for the function "<<funcName<<" against good behavior # "<<behaviorID<<": "<<endl;
	ss<<"  P(I): " <<PofI<< endl;
	ss<<"  Q(I,O): " <<QofO<< endl;
	if (PofI && QofO)
	{
		ss<<"Actual: P AND Q"<<endl;
		ss<<"Required: (NOT P) OR Q"<<endl;
		ss<<"Suggested Correction: choosing one of the following options:"<<endl;
		ss<<"1. Strengthen P so that P(I) = false."<<endl;
		ss<<"2. Skip."<<endl;
	}
	else if (PofI && !QofO)
	{
		ss<<"Actual: P AND (NOT Q)"<<endl;
		ss<<"Required: (NOT P) OR Q"<<endl;
		ss<<"Suggested Correction: choosing only one of the following options:"<<endl;
		ss<<"1. Strengthen P so that P(I) = false."<<endl;
		ss<<"2. Weaken Q so that Q(I,O) = true."<<endl;
	}
	else if (!PofI && QofO)
	{
		ss<<"Actual: (NOT P) AND Q"<<endl;
		ss<<"Required: (NOT P) OR Q"<<endl;
		ss<<"Suggested Correction: choosing only one of the following options:"<<endl;
		ss<<"1. Weaken P so that P(I) = true."<<endl;
		ss<<"2. Strengthen Q so that Q(I,O) = false."<<endl;
		ss<<"3. Skip."<<endl;
	}
	else if (!PofI && !QofO)
	{
		ss<<"Actual: (NOT P) AND (NOT Q)"<<endl;
		ss<<"Required: (NOT P) OR Q"<<endl;
		ss<<"Suggested Correction: choosing one of the following options:"<<endl;
		ss<<"1. Weaken P so that P(I) = true, and strengthen Q so that Q(I,O) = false."<<endl;
		ss<<"2. Skip."<<endl;
	}
	ss<<"============"<<endl<<endl;
	cout<<ss.str();
}

void PDTSpecCheck::checkBad(PDTFunctionDec& functionDec,
        PDTPreCondition& preCondition,
        PDTPostCondition& postCondition,
        PDTBehaviors& behaviors,
        const string & funcName, 
        int behaviorID)
{
	behaviors.assignBadInput(*CG, behaviorID);
	preCondition.eval(*CG);
	behaviors.assignBadOutput(*CG, behaviorID);
	postCondition.eval(*CG);

	//SPEC CHECK:
	bool PofI = (dynamic_cast<PDTBoolConst*>(preCondition.nValue))->getValue();
	bool QofO = (dynamic_cast<PDTBoolConst*>(postCondition.nValue))->getValue();
	stringstream ss(stringstream::in | stringstream::out);
	ss<<endl;
	ss<<"============"<<endl;
	ss<<"Final Result"<<endl;
	ss<<"============"<<endl;
	ss<<"Spec Check result for the function "<<funcName<<" against bad behavior # "<<behaviorID<<": "<<endl;
	ss<<"  P(I): " <<PofI<< endl;
	ss<<"  Q(O): " <<QofO<< endl;
	if (PofI && QofO)
	{
		ss<<"Actual: P AND Q"<<endl;
		ss<<"Required: P AND (NOT Q)"<<endl;
		ss<<"Suggested Correction: Strengthen Q so that Q(I,O) = false."<<endl;
	}
	else if (PofI && !QofO)
	{
		ss<<"Actual: P AND (NOT Q)"<<endl;
		ss<<"Required: P AND (NOT Q)"<<endl;
		ss<<"Not corrections needed: "<<endl;
	}
	else if (!PofI && QofO)
	{
		ss<<"Actual: (NOT P) AND Q"<<endl;
		ss<<"Required: P AND (NOT Q)"<<endl;
		ss<<"Suggested Correction: Weaken P so that P(I) = true, and strengthen Q so that Q(I,O) = false"<<endl;
	}
	else if (!PofI && !QofO)
	{
		ss<<"Actual: (NOT P) AND (NOT Q)"<<endl;
		ss<<"Required: P AND (NOT Q)"<<endl;
		ss<<"Suggested Correction: Weaken P so that P(I) = true"<<endl;
	}
	ss<<"============"<<endl<<endl;
	cout<<ss.str();
}

void PDTSpecCheck::checkAllGood(PDTFunctionDec& functionDec,
        PDTPreCondition& preCondition,
        PDTPostCondition& postCondition,
        PDTBehaviors& behaviors,
        const string & funcName)
{
    stringstream ss(stringstream::in | stringstream::out);
    ss<<endl;
    ss<<"============"<<endl;
    ss<<"Final Result"<<endl;
    ss<<"============"<<endl;
    ss<<"Spec Check result for the function "<<funcName<<" against the following good behaviors: "<<endl;
    for (int i = 0; i < behaviors.getGoodSize(); i++)
    {
        behaviors.assignGoodInput(*CG, i);
        preCondition.eval(*CG);
        behaviors.assignGoodOutput(*CG, i);
        postCondition.eval(*CG);
        ss<<"Behavior ID # "<<i<<": "<<endl;
        bool PofI = (dynamic_cast<PDTBoolConst*>(preCondition.nValue))->getValue();
        bool QofO = (dynamic_cast<PDTBoolConst*>(postCondition.nValue))->getValue();
        ss<<"  P(I): " <<PofI<< endl;
        ss<<"  Q(O): " <<QofO<< endl;
        if (PofI && QofO)
        {
            ss<<"Actual: P AND Q"<<endl;
            ss<<"Required: (NOT P) OR Q"<<endl;
            ss<<"Suggested Correction: choosing one of the following options:"<<endl;
            ss<<"1. Strengthen P so that P(I) = false."<<endl;
            ss<<"2. Skip."<<endl;
        }
        else if (PofI && !QofO)
        {
            ss<<"Actual: P AND (NOT Q)"<<endl;
            ss<<"Required: (NOT P) OR Q"<<endl;
            ss<<"Suggested Correction: choosing only one of the following options:"<<endl;
            ss<<"1. Strengthen P so that P(I) = false."<<endl;
            ss<<"2. Weaken Q so that Q(I,O) = true."<<endl;
        }
        else if (!PofI && QofO)
        {
            ss<<"Actual: (NOT P) AND Q"<<endl;
            ss<<"Required: (NOT P) OR Q"<<endl;
            ss<<"Suggested Correction: choosing only one of the following options:"<<endl;
            ss<<"1. Weaken P so that P(I) = true."<<endl;
            ss<<"2. Strengthen Q so that Q(I,O) = false."<<endl;
            ss<<"3. Skip."<<endl;
        }
        else if (!PofI && !QofO)
        {
            ss<<"Actual: (NOT P) AND (NOT Q)"<<endl;
            ss<<"Required: (NOT P) OR Q"<<endl;
            ss<<"Suggested Correction: choosing one of the following options:"<<endl;
            ss<<"1. Weaken P so that P(I) = true, and strengthen Q so that Q(I,O) = false."<<endl;
            ss<<"2. Skip."<<endl;
        }
    }
    ss<<"============"<<endl<<endl;
    cout<<ss.str();
}

void PDTSpecCheck::checkAllBad(PDTFunctionDec& functionDec,
        PDTPreCondition& preCondition,
        PDTPostCondition& postCondition,
        PDTBehaviors& behaviors,
        const string & funcName)
{
	stringstream ss(stringstream::in | stringstream::out);
	ss<<endl;
	ss<<"============"<<endl;
	ss<<"Final Result"<<endl;
	ss<<"============"<<endl;
	ss<<"Spec Check result for the function "<<funcName<<" against the following bad behaviors: "<<endl;
	for (int i = 0; i < behaviors.getBadSize(); i++)
	{
		behaviors.assignBadInput(*CG, i);
		preCondition.eval(*CG);
		behaviors.assignBadOutput(*CG, i);
		postCondition.eval(*CG);

		ss<<"Behavior ID # "<<i<<": "<<endl;
		bool PofI = (dynamic_cast<PDTBoolConst*>(preCondition.nValue))->getValue();
		bool QofO = (dynamic_cast<PDTBoolConst*>(postCondition.nValue))->getValue();
		ss<<"  P(I): " <<PofI<< endl;
		ss<<"  Q(O): " <<QofO<< endl;
		if (PofI && QofO)
		{
			ss<<"Actual: P AND Q"<<endl;
			ss<<"Required: P AND (NOT Q)"<<endl;
			ss<<"Suggested Correction: Strengthen Q so that Q(I,O) = false."<<endl;
		}
		else if (PofI && !QofO)
		{
			ss<<"Actual: P AND (NOT Q)"<<endl;
			ss<<"Required: P AND (NOT Q)"<<endl;
			ss<<"Not corrections needed: "<<endl;
		}
		else if (!PofI && QofO)
		{
			ss<<"Actual: (NOT P) AND Q"<<endl;
			ss<<"Required: P AND (NOT Q)"<<endl;
			ss<<"Suggested Correction: Weaken P so that P(I) = true, and strengthen Q so that Q(I,O) = false"<<endl;
		}
		else if (!PofI && !QofO)
		{
			ss<<"Actual: (NOT P) AND (NOT Q)"<<endl;
			ss<<"Required: P AND (NOT Q)"<<endl;
			ss<<"Suggested Correction: Weaken P so that P(I) = true"<<endl;
		}
	}
	ss<<"============"<<endl<<endl;
	cout<<ss.str();
}

void 
PDTSpecCheck::
checkAll(PDTFunctionDec& functionDec,
        PDTPreCondition& preCondition,
        PDTPostCondition& postCondition,
        PDTBehaviors& behaviors,
        const string & funcName)
{
	stringstream ss(stringstream::in | stringstream::out);
	ss<<endl;
	ss<<"============================"<<endl;
	ss<<"Final Result: Good Behaviors"<<endl;
	ss<<"============================"<<endl;
	ss<<"Spec Check result for the function "<<funcName<<" against the following good behaviors: "<<endl;
	for (int i = 0; i<behaviors.getGoodSize(); i++)
	{
		behaviors.assignGoodInput(*CG, i);
		preCondition.eval(*CG);
		behaviors.assignGoodOutput(*CG, i);
		postCondition.eval(*CG);

		ss<<"Behavior ID # "<<i<<": "<<endl;
		bool PofI = (dynamic_cast<PDTBoolConst*>(preCondition.nValue))->getValue();
		bool QofO = (dynamic_cast<PDTBoolConst*>(postCondition.nValue))->getValue();
		ss<<"  P(I): " <<PofI<< endl;
		ss<<"  Q(O): " <<QofO<< endl;
		if (PofI && QofO)
		{
			ss<<"Actual: P AND Q"<<endl;
			ss<<"Required: (NOT P) OR Q"<<endl;
			ss<<"Suggested Correction: choosing one of the following options:"<<endl;
			ss<<"1. Strengthen P so that P(I) = false."<<endl;
			ss<<"2. Skip."<<endl;
		}
		else if (PofI && !QofO)
		{
			ss<<"Actual: P AND (NOT Q)"<<endl;
			ss<<"Required: (NOT P) OR Q"<<endl;
			ss<<"Suggested Correction: choosing only one of the following options:"<<endl;
			ss<<"1. Strengthen P so that P(I) = false."<<endl;
			ss<<"2. Weaken Q so that Q(I,O) = true."<<endl;
		}
		else if (!PofI && QofO)
		{
			ss<<"Actual: (NOT P) AND Q"<<endl;
			ss<<"Required: (NOT P) OR Q"<<endl;
			ss<<"Suggested Correction: choosing only one of the following options:"<<endl;
			ss<<"1. Weaken P so that P(I) = true."<<endl;
			ss<<"2. Strengthen Q so that Q(I,O) = false."<<endl;
			ss<<"3. Skip."<<endl;
		}
		else if (!PofI && !QofO)
		{
			ss<<"Actual: (NOT P) AND (NOT Q)"<<endl;
			ss<<"Required: (NOT P) OR Q"<<endl;
			ss<<"Suggested Correction: choosing one of the following options:"<<endl;
			ss<<"1. Weaken P so that P(I) = true, and strengthen Q so that Q(I,O) = false."<<endl;
			ss<<"2. Skip."<<endl;
		}
	}

	ss<<"============================"<<endl;
	ss<<endl;
	ss<<"============================"<<endl;
	ss<<"Final Result:  Bad Behaviors"<<endl;
	ss<<"============================"<<endl;
	ss<<"Spec Check result for the function "<<funcName<<" against the following bad behaviors: "<<endl;
	for (int i = 0; i<behaviors.getBadSize(); i++)
	{
		behaviors.assignBadInput(*CG, i);
		preCondition.eval(*CG);
		behaviors.assignBadOutput(*CG, i);
		postCondition.eval(*CG);

		ss<<"Behavior ID # "<<i<<": "<<endl;
		bool PofI = (dynamic_cast<PDTBoolConst*>(preCondition.nValue))->getValue();
		bool QofO = (dynamic_cast<PDTBoolConst*>(postCondition.nValue))->getValue();
		ss<<"  P(I): " <<PofI<< endl;
		ss<<"  Q(O): " <<QofO<< endl;
		if (PofI && QofO)
		{
			ss<<"Actual: P AND Q"<<endl;
			ss<<"Required: P AND (NOT Q)"<<endl;
			ss<<"Suggested Correction: Strengthen Q so that Q(I,O) = false."<<endl;
		}
		else if (PofI && !QofO)
		{
			ss<<"Actual: P AND (NOT Q)"<<endl;
			ss<<"Required: P AND (NOT Q)"<<endl;
			ss<<"Not corrections needed: "<<endl;
		}
		else if (!PofI && QofO)
		{
			ss<<"Actual: (NOT P) AND Q"<<endl;
			ss<<"Required: P AND (NOT Q)"<<endl;
			ss<<"Suggested Correction: Weaken P so that P(I) = true, and strengthen Q so that Q(I,O) = false"<<endl;
		}
		else if (!PofI && !QofO)
		{
			ss<<"Actual: (NOT P) AND (NOT Q)"<<endl;
			ss<<"Required: P AND (NOT Q)"<<endl;
			ss<<"Suggested Correction: Weaken P so that P(I) = true"<<endl;
		}
	}
	ss<<"============================"<<endl;
	cout<<ss.str();
}

PDTListOfStatements& 
PDTSpecCheck::getFunctionCode(PDTFunctionDec& functionDec)
{
    //TODO: why are we copying code here?
	PDTListOfStatements* allStatments = functionDec.getStatements();
	vector<PDTStatement*> newStatementList;
	cout<<endl;

	for (unsigned int i = 0; i<allStatments->numberOfStmts(); i++)
	{
		if (!allStatments->getStatmentAt(i)->isPreCondition()
		 && !allStatments->getStatmentAt(i)->isPostCondition()
		 && !allStatments->getStatmentAt(i)->isBehaviors())
		{
			//add to a new list of stmts:
			newStatementList.push_back(allStatments->getStatmentAt(i));
		}
	}
	PDTListOfStatements* toReturn = new PDTListOfStatements(*CG, newStatementList);
	stringstream ss(stringstream::in | stringstream::out);
	if (toReturn->numberOfStmts()>0)
	{
		ss<<"=========================================================="<<endl;
		ss<<"                     Program Code                         "<<endl;
		ss<<"=========================================================="<<endl;
		for (unsigned int i = 0; i<toReturn->numberOfStmts(); i++)
			toReturn->getStatmentAt(i)->toString(ss);
		ss<<"=========================================================="<<endl;
		cout<<ss.str()<<endl;
	}

	return *toReturn;
}

bool PDTSpecCheck::nValueEqual(PDTNode* node1, PDTNode* node2) //Compare two nodes
{
	if (node1->isNumConstInt() && node2->isNumConstInt())
	{
		int node1Val = (dynamic_cast<PDTNumConstInt*>(node1))->getValue();
		int node2Val = (dynamic_cast<PDTNumConstInt*>(node2))->getValue();
			return node1Val == node2Val;
	}
	else if (node1->isBoolConst() && node2->isBoolConst())
	{
		bool node1Val = (dynamic_cast<PDTBoolConst*>(node1))->getValue();
		bool node2Val = (dynamic_cast<PDTBoolConst*>(node2))->getValue();
			return node1Val == node2Val;
	}
	else if (node1->isConstSequence() && node2->isConstSequence()) //if seq const, compare elem by elem
	{
		PDTConstSequence* seq1 = dynamic_cast<PDTConstSequence*>(node1);
		PDTConstSequence* seq2 = dynamic_cast<PDTConstSequence*>(node2);
		for (unsigned int i = 0; i<seq1->getSize(); i++)
			if (!(nValueEqual(seq1->getElementAt(i), seq2->getElementAt(i))))
				return false;
		return true;
	}
	else
		return false;
}

void PDTSpecCheck::
checkWithCode( PDTFunctionDec& functionDec,
        PDTPreCondition& preCondition,
        PDTPostCondition& postCondition,
        PDTBehaviors& behaviors,
        const string & funcName)
{ try {
	PDTListOfStatements& funcCode = getFunctionCode(functionDec);
	stringstream ss(stringstream::in | stringstream::out);
	ss<<"===================================================================="<<endl;
	ss<<"Final Result: Computing adequacy for 'GOOD' behaviors for {P}S{Q}{B}"<<endl;
	ss<<"===================================================================="<<endl;

	vector <PDTBehavior*> goodAssignments;
	goodAssignments = behaviors.getGoodAssignments(goodAssignments); //All good behaviors

	for (int i = 0; i<behaviors.getGoodSize(); i++)
	{
		//assigning input and output and finding pre and post conditions
		behaviors.assignGoodInput(*CG, i);
		preCondition.eval(*CG);
		behaviors.assignGoodOutput(*CG, i);
		postCondition.eval(*CG);

		//finding the vector of output variables
		vector <PDTVar*> outVarVec;
		outVarVec = goodAssignments[0]->getOutputVariables(outVarVec);

		//finding the vector of values of the output variables
		vector <PDTNode*> outValuesVec1;
		for (unsigned int j = 0; j<outVarVec.size(); j++)
			outValuesVec1.push_back(outVarVec[j]->getValue());

		//Finding boolean P(I) and Q(O)
		bool PofI = (dynamic_cast<PDTBoolConst*>(preCondition.nValue))->getValue();
		bool QofO = (dynamic_cast<PDTBoolConst*>(postCondition.nValue))->getValue();

		behaviors.assignGoodInput(*CG, i);
		//Executing S and evaluating post condition again
		funcCode.eval(*CG);
		postCondition.eval(*CG);
		//finding the vector of values of the output variables after running S
		vector <PDTNode*> outValuesVec2;
		for (unsigned int j = 0; j<outVarVec.size(); j++)
			outValuesVec2.push_back(outVarVec[j]->getValue());

		//finding boolean Q(O')
		bool QofOPrime = (dynamic_cast<PDTBoolConst*>(postCondition.nValue))->getValue();

		//finding if O==O'
		bool equality = true;
		for (unsigned int j = 0; j<outValuesVec1.size(); j++)
		{
			if (!(nValueEqual(outValuesVec1[j], outValuesVec2[j])))
				equality = false;
		}

		ss<<"Behavior ID # "<<i<<": " << endl;
		ss<<"  P(I): " <<PofI<< endl;
		ss<<"  Q(O): " <<QofO<< endl;
		ss<<"  Q(O'): " <<QofOPrime<< endl;

		if (equality)
		{
			ss<<"  O and O' are the same"<<endl;
			ss<<"  O' in g(i)"<<endl;
			if (QofOPrime)
			{
				ss<<"  O' in VQ(i)"<<endl;
				ss<<"  No correction needed"<<endl;
			}
			if (!QofOPrime)
			{
				ss<<"  O' is not in VQ(i)"<<endl;
				ss<<"  Suggested Correction: Weaken Q so that Q(I, O) = true"<<endl;
			}
		}

		else
		{
			ss<<"  O and O' are not the same"<<endl;
			ss<<"  O' is not in g(i)"<<endl;
			if (QofOPrime)
			{
				ss<<"  O' in VQ(i)"<<endl;
				ss<<"  Suggested Correction: Strengthen Q so that Q(I, O) = false, and modify S so that O' is not in  S(I)"<<endl;
			}
			if (!QofOPrime)
			{
				ss<<"  O' is not in VQ(i)"<<endl;
				ss<<"  Suggested Correction: Modify S so that O' is not in  S(I)"<<endl;
			}
		}
	}
	ss<<"===================================================================="<<endl;

	ss<<endl;

	ss<<"===================================================================="<<endl;
	ss<<"Final Result:  Computing adequacy for 'BAD' behaviors for {P}S{Q}{B}"<<endl;
	ss<<"===================================================================="<<endl;

	vector <PDTBehavior*> badAssignments;
	badAssignments = behaviors.getBadAssignments(badAssignments); //All good behaviors

	for (int i = 0; i<behaviors.getBadSize(); i++)
	{
		//assigning input and output and finding pre and post conditions
		behaviors.assignBadInput(*CG, i);
		preCondition.eval(*CG);
		behaviors.assignBadOutput(*CG, i);
		postCondition.eval(*CG);

		//finding the vector of output variables
		vector <PDTVar*> outVarVec;
		outVarVec = badAssignments[0]->getOutputVariables(outVarVec);

		//finding the vector of values of the output variables
		vector <PDTNode*> outValuesVec1;
		for (unsigned int j = 0; j<outVarVec.size(); j++)
			outValuesVec1.push_back(outVarVec[j]->getValue());

		//Finding boolean P(I) and Q(O)
		bool PofI = (dynamic_cast<PDTBoolConst*>(preCondition.nValue))->getValue();
		bool QofO = (dynamic_cast<PDTBoolConst*>(postCondition.nValue))->getValue();

		behaviors.assignBadInput(*CG, i);
		//Executing S and evaluating post condition again
		funcCode.eval(*CG);
		postCondition.eval(*CG);

		//finding the vector of values of the output variables after running S
		vector <PDTNode*> outValuesVec2;
		for (unsigned int j = 0; j<outVarVec.size(); j++)
			outValuesVec2.push_back(outVarVec[j]->getValue());

		//finding boolean Q(O')
		bool QofOPrime = (dynamic_cast<PDTBoolConst*>(postCondition.nValue))->getValue();

		//finding if O==O'
		bool equality = true;
		for (unsigned int j = 0; j<outValuesVec1.size(); j++)
		{
			if (!(nValueEqual(outValuesVec1[j], outValuesVec2[j])))
				equality = false;
		}

		ss<<"Behavior ID # "<<i<<": " << endl;
		ss<<"  P(I): " <<PofI<< endl;
		ss<<"  Q(O): " <<QofO<< endl;
		ss<<"  Q(O'): " <<QofOPrime<< endl;

		if (!equality) //DONT KNOW??
		{
			ss<<"  O and O' are not the same"<<endl;

		}

		else //equality => bad behavior
		{
			ss<<"  O and O' are the same"<<endl;
			ss<<"  O' is in g(i)"<<endl;
			if (QofOPrime)
			{
				ss<<"  O' in VQ(i)"<<endl;
				ss<<"  Suggested Correction: Strengthen Q so that Q(I, O) = false, and modify S so that O' is not in  S(I)"<<endl;
			}
			if (!QofOPrime)
			{
				ss<<"  O' is not in VQ(i)"<<endl;
				ss<<"  Suggested Correction: Modify S so that O' is not in  S(I)"<<endl;
			}
		}
	}
	ss<<"===================================================================="<<endl;
	cout<<ss.str()<<endl;
      }catch (PDTNodeException e) {
          if (e == PDTNullValEx) {
              cerr << "Null value met. Check whether you missed a variable initialization in the behavior." << endl;
          }
      }
}

void 
PDTSpecCheck::check(string func, string spec)
{
    PDTFunctionDec * functionDec = CG->findFunction(func);

    if (functionDec == NULL)
    {
        cerr <<"Function " << func << " not found!" << endl;
        return;
    }
    if (func.empty())
        func = functionDec->getName();

    PDTBehaviors* behaviors = functionDec->findBehaviors(spec);
    if (behaviors == NULL) {
        cerr << "No behavior [" << spec << "] defined for function " << func << "!" << endl;
        return;
    }
    if (spec.empty()) 
        spec = behaviors->getName();

    PDTPreCondition* preCondition = functionDec->findPre(spec);
    PDTPostCondition* postCondition = functionDec->findPost(spec);
    PDTListOfStatements& funcCode = getFunctionCode(*functionDec);

    bool preExists = !(preCondition == NULL) && !(preCondition->getChildren().size() == 0);
    bool postExists = !(postCondition == NULL)  && !(postCondition->getChildren().size() == 0);
    bool behaviorsExists = !(behaviors == NULL) && !(behaviors->getChildren().size() == 0);
    bool codeExists = (funcCode.numberOfStmts() > 0);

    if (!preExists && !postCondition && behaviorsExists) //Just compute the ranges
    {
        //TODO: Which range to choose?

        //vector <PDTIntRange*> rangesGood;
        //vector <PDTVar*> variablesGood;
        //this->buildRangesGood(func, rangesGood, variablesGood);

        //vector <PDTIntRange*> rangesBad;
        //vector <PDTVar*> variablesBad;
        //this->buildRangesBad(func, rangesBad, variablesBad);

        vector <PDTIntRange*> rangesAll;
        vector <PDTVar*> variablesAll;
        buildAllRanges(*functionDec, *behaviors, func, 
                rangesAll, variablesAll);
        return;
    }

    if (preExists && postExists && behaviorsExists && !codeExists) //Table 1
    {
        checkAll(*functionDec, *preCondition,*postCondition,*behaviors,func);
        return;
    }

    if (preExists && postExists && behaviorsExists && codeExists) //Adequacy Check - All tables
    {
        checkWithCode(*functionDec, *preCondition,*postCondition,*behaviors,func);
        return;
    }
}
